A:Type, es:ES, I:AbsInterface(A), P:(E), p:(e:E. Dec(P(e))).
(e:E. ((e  I))  P(e))  ((I|p) = I) 

latex

Definitions	X(e), f(a), x(s), (I|p), <a, b>, s = t, x:A. B(x), b, P  Q, E, e  X, t  T, P  Q, P & Q, P  Q, x.A(x), x. t(x), Type, ES, AbsInterface(A), , x:AB(x), Dec(P), x:A  B(x), t.1, if b then t else f fi , A c B, A, let x,y = A in B(x;y)
Lemmas	es-interface-val-restrict, es-interface-val wf, es-is-interface-restrict, decidable wf, es-E wf, es-interface wf, event system wf, es-interface-extensionality, es-interface-restrict wf, assert wf, es-is-interface wf